ds:fpf(Id; x.Type), es:event_system{i:l}, i:Id.
@i discrete ds
 (t:rationals. es-init-elapsed(es; i; t) = es-init-state(es; i)  decl-state(ds)) 

latex

Definitions

t  T, P  Q, x:A. B(x), es-state(es; i), decl-state(ds), es-init-state(es; i), ma-state(ds), x:AB(x), es-init-elapsed(es; i; t), atom{$n:n}, Type, x:A  B(x), fpf(A; a.B(a)), event_system{i:l}, Id, fpf-all(A; eq; f; x,v.P(x;v)), @i discrete ds, quotient(A; x,y.B(x;y)), rationals, f(a), <a, b>, top, fpf-cap(f; eq; x; z), s = t, x. t(x), fpf-ap(f; eq; x), es-dtype(es; i; x; T), id-deq, x.A(x), void, isect(A; x.B(x)), b, A, b, , prop{i:l}, if b then t else f fi , fpf-dom(eq; x; f), P  Q, P  Q, Unit, left + right, es-vartype(es; i; x), case b of inl(x) => s(x) | inr(y) => t(y)

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, equal-top, discrete-init-elapsed, fpf-ap wf, id-deq wf, rationals wf, es-dds wf, event system wf, fpf wf, Id wf, es-init-elapsed wf, es-init-state wf, es-state-subtype2